Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__from1(X) -> cons2(mark1(X), from1(s1(X)))
a__2ndspos2(0, Z) -> rnil
a__2ndspos2(s1(N), cons2(X, Z)) -> a__2ndspos2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndspos2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(posrecip1(mark1(Y)), a__2ndsneg2(mark1(N), mark1(Z)))
a__2ndsneg2(0, Z) -> rnil
a__2ndsneg2(s1(N), cons2(X, Z)) -> a__2ndsneg2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndsneg2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(negrecip1(mark1(Y)), a__2ndspos2(mark1(N), mark1(Z)))
a__pi1(X) -> a__2ndspos2(mark1(X), a__from1(0))
a__plus2(0, Y) -> mark1(Y)
a__plus2(s1(X), Y) -> s1(a__plus2(mark1(X), mark1(Y)))
a__times2(0, Y) -> 0
a__times2(s1(X), Y) -> a__plus2(mark1(Y), a__times2(mark1(X), mark1(Y)))
a__square1(X) -> a__times2(mark1(X), mark1(X))
mark1(from1(X)) -> a__from1(mark1(X))
mark1(2ndspos2(X1, X2)) -> a__2ndspos2(mark1(X1), mark1(X2))
mark1(2ndsneg2(X1, X2)) -> a__2ndsneg2(mark1(X1), mark1(X2))
mark1(pi1(X)) -> a__pi1(mark1(X))
mark1(plus2(X1, X2)) -> a__plus2(mark1(X1), mark1(X2))
mark1(times2(X1, X2)) -> a__times2(mark1(X1), mark1(X2))
mark1(square1(X)) -> a__square1(mark1(X))
mark1(0) -> 0
mark1(s1(X)) -> s1(mark1(X))
mark1(posrecip1(X)) -> posrecip1(mark1(X))
mark1(negrecip1(X)) -> negrecip1(mark1(X))
mark1(nil) -> nil
mark1(cons2(X1, X2)) -> cons2(mark1(X1), X2)
mark1(cons22(X1, X2)) -> cons22(X1, mark1(X2))
mark1(rnil) -> rnil
mark1(rcons2(X1, X2)) -> rcons2(mark1(X1), mark1(X2))
a__from1(X) -> from1(X)
a__2ndspos2(X1, X2) -> 2ndspos2(X1, X2)
a__2ndsneg2(X1, X2) -> 2ndsneg2(X1, X2)
a__pi1(X) -> pi1(X)
a__plus2(X1, X2) -> plus2(X1, X2)
a__times2(X1, X2) -> times2(X1, X2)
a__square1(X) -> square1(X)

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__from1(X) -> cons2(mark1(X), from1(s1(X)))
a__2ndspos2(0, Z) -> rnil
a__2ndspos2(s1(N), cons2(X, Z)) -> a__2ndspos2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndspos2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(posrecip1(mark1(Y)), a__2ndsneg2(mark1(N), mark1(Z)))
a__2ndsneg2(0, Z) -> rnil
a__2ndsneg2(s1(N), cons2(X, Z)) -> a__2ndsneg2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndsneg2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(negrecip1(mark1(Y)), a__2ndspos2(mark1(N), mark1(Z)))
a__pi1(X) -> a__2ndspos2(mark1(X), a__from1(0))
a__plus2(0, Y) -> mark1(Y)
a__plus2(s1(X), Y) -> s1(a__plus2(mark1(X), mark1(Y)))
a__times2(0, Y) -> 0
a__times2(s1(X), Y) -> a__plus2(mark1(Y), a__times2(mark1(X), mark1(Y)))
a__square1(X) -> a__times2(mark1(X), mark1(X))
mark1(from1(X)) -> a__from1(mark1(X))
mark1(2ndspos2(X1, X2)) -> a__2ndspos2(mark1(X1), mark1(X2))
mark1(2ndsneg2(X1, X2)) -> a__2ndsneg2(mark1(X1), mark1(X2))
mark1(pi1(X)) -> a__pi1(mark1(X))
mark1(plus2(X1, X2)) -> a__plus2(mark1(X1), mark1(X2))
mark1(times2(X1, X2)) -> a__times2(mark1(X1), mark1(X2))
mark1(square1(X)) -> a__square1(mark1(X))
mark1(0) -> 0
mark1(s1(X)) -> s1(mark1(X))
mark1(posrecip1(X)) -> posrecip1(mark1(X))
mark1(negrecip1(X)) -> negrecip1(mark1(X))
mark1(nil) -> nil
mark1(cons2(X1, X2)) -> cons2(mark1(X1), X2)
mark1(cons22(X1, X2)) -> cons22(X1, mark1(X2))
mark1(rnil) -> rnil
mark1(rcons2(X1, X2)) -> rcons2(mark1(X1), mark1(X2))
a__from1(X) -> from1(X)
a__2ndspos2(X1, X2) -> 2ndspos2(X1, X2)
a__2ndsneg2(X1, X2) -> 2ndsneg2(X1, X2)
a__pi1(X) -> pi1(X)
a__plus2(X1, X2) -> plus2(X1, X2)
a__times2(X1, X2) -> times2(X1, X2)
a__square1(X) -> square1(X)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK1(2ndspos2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> A__2NDSPOS2(mark1(N), mark1(Z))
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> A__2NDSNEG2(mark1(N), mark1(Z))
A__PI1(X) -> A__2NDSPOS2(mark1(X), a__from1(0))
MARK1(plus2(X1, X2)) -> MARK1(X2)
A__TIMES2(s1(X), Y) -> A__TIMES2(mark1(X), mark1(Y))
MARK1(negrecip1(X)) -> MARK1(X)
MARK1(rcons2(X1, X2)) -> MARK1(X1)
A__TIMES2(s1(X), Y) -> MARK1(X)
MARK1(times2(X1, X2)) -> MARK1(X2)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> A__2NDSNEG2(s1(mark1(N)), cons22(X, mark1(Z)))
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(N)
MARK1(plus2(X1, X2)) -> A__PLUS2(mark1(X1), mark1(X2))
A__2NDSPOS2(s1(N), cons2(X, Z)) -> A__2NDSPOS2(s1(mark1(N)), cons22(X, mark1(Z)))
MARK1(posrecip1(X)) -> MARK1(X)
MARK1(times2(X1, X2)) -> A__TIMES2(mark1(X1), mark1(X2))
A__PI1(X) -> MARK1(X)
A__2NDSPOS2(s1(N), cons2(X, Z)) -> MARK1(Z)
MARK1(s1(X)) -> MARK1(X)
MARK1(rcons2(X1, X2)) -> MARK1(X2)
MARK1(2ndspos2(X1, X2)) -> A__2NDSPOS2(mark1(X1), mark1(X2))
MARK1(2ndsneg2(X1, X2)) -> A__2NDSNEG2(mark1(X1), mark1(X2))
A__2NDSPOS2(s1(N), cons2(X, Z)) -> MARK1(N)
MARK1(pi1(X)) -> MARK1(X)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(N)
A__SQUARE1(X) -> MARK1(X)
A__FROM1(X) -> MARK1(X)
MARK1(plus2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Y)
A__TIMES2(s1(X), Y) -> A__PLUS2(mark1(Y), a__times2(mark1(X), mark1(Y)))
MARK1(times2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> MARK1(N)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> MARK1(Z)
MARK1(cons22(X1, X2)) -> MARK1(X2)
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Z)
A__PLUS2(s1(X), Y) -> A__PLUS2(mark1(X), mark1(Y))
MARK1(from1(X)) -> MARK1(X)
A__PI1(X) -> A__FROM1(0)
MARK1(from1(X)) -> A__FROM1(mark1(X))
MARK1(pi1(X)) -> A__PI1(mark1(X))
MARK1(cons2(X1, X2)) -> MARK1(X1)
A__SQUARE1(X) -> A__TIMES2(mark1(X), mark1(X))
A__PLUS2(0, Y) -> MARK1(Y)
MARK1(2ndspos2(X1, X2)) -> MARK1(X2)
A__PLUS2(s1(X), Y) -> MARK1(X)
MARK1(square1(X)) -> MARK1(X)
MARK1(2ndsneg2(X1, X2)) -> MARK1(X1)
MARK1(square1(X)) -> A__SQUARE1(mark1(X))
A__PLUS2(s1(X), Y) -> MARK1(Y)
MARK1(2ndsneg2(X1, X2)) -> MARK1(X2)
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Y)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Z)
A__TIMES2(s1(X), Y) -> MARK1(Y)

The TRS R consists of the following rules:

a__from1(X) -> cons2(mark1(X), from1(s1(X)))
a__2ndspos2(0, Z) -> rnil
a__2ndspos2(s1(N), cons2(X, Z)) -> a__2ndspos2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndspos2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(posrecip1(mark1(Y)), a__2ndsneg2(mark1(N), mark1(Z)))
a__2ndsneg2(0, Z) -> rnil
a__2ndsneg2(s1(N), cons2(X, Z)) -> a__2ndsneg2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndsneg2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(negrecip1(mark1(Y)), a__2ndspos2(mark1(N), mark1(Z)))
a__pi1(X) -> a__2ndspos2(mark1(X), a__from1(0))
a__plus2(0, Y) -> mark1(Y)
a__plus2(s1(X), Y) -> s1(a__plus2(mark1(X), mark1(Y)))
a__times2(0, Y) -> 0
a__times2(s1(X), Y) -> a__plus2(mark1(Y), a__times2(mark1(X), mark1(Y)))
a__square1(X) -> a__times2(mark1(X), mark1(X))
mark1(from1(X)) -> a__from1(mark1(X))
mark1(2ndspos2(X1, X2)) -> a__2ndspos2(mark1(X1), mark1(X2))
mark1(2ndsneg2(X1, X2)) -> a__2ndsneg2(mark1(X1), mark1(X2))
mark1(pi1(X)) -> a__pi1(mark1(X))
mark1(plus2(X1, X2)) -> a__plus2(mark1(X1), mark1(X2))
mark1(times2(X1, X2)) -> a__times2(mark1(X1), mark1(X2))
mark1(square1(X)) -> a__square1(mark1(X))
mark1(0) -> 0
mark1(s1(X)) -> s1(mark1(X))
mark1(posrecip1(X)) -> posrecip1(mark1(X))
mark1(negrecip1(X)) -> negrecip1(mark1(X))
mark1(nil) -> nil
mark1(cons2(X1, X2)) -> cons2(mark1(X1), X2)
mark1(cons22(X1, X2)) -> cons22(X1, mark1(X2))
mark1(rnil) -> rnil
mark1(rcons2(X1, X2)) -> rcons2(mark1(X1), mark1(X2))
a__from1(X) -> from1(X)
a__2ndspos2(X1, X2) -> 2ndspos2(X1, X2)
a__2ndsneg2(X1, X2) -> 2ndsneg2(X1, X2)
a__pi1(X) -> pi1(X)
a__plus2(X1, X2) -> plus2(X1, X2)
a__times2(X1, X2) -> times2(X1, X2)
a__square1(X) -> square1(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP

Q DP problem:
The TRS P consists of the following rules:

MARK1(2ndspos2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> A__2NDSPOS2(mark1(N), mark1(Z))
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> A__2NDSNEG2(mark1(N), mark1(Z))
A__PI1(X) -> A__2NDSPOS2(mark1(X), a__from1(0))
MARK1(plus2(X1, X2)) -> MARK1(X2)
A__TIMES2(s1(X), Y) -> A__TIMES2(mark1(X), mark1(Y))
MARK1(negrecip1(X)) -> MARK1(X)
MARK1(rcons2(X1, X2)) -> MARK1(X1)
A__TIMES2(s1(X), Y) -> MARK1(X)
MARK1(times2(X1, X2)) -> MARK1(X2)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> A__2NDSNEG2(s1(mark1(N)), cons22(X, mark1(Z)))
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(N)
MARK1(plus2(X1, X2)) -> A__PLUS2(mark1(X1), mark1(X2))
A__2NDSPOS2(s1(N), cons2(X, Z)) -> A__2NDSPOS2(s1(mark1(N)), cons22(X, mark1(Z)))
MARK1(posrecip1(X)) -> MARK1(X)
MARK1(times2(X1, X2)) -> A__TIMES2(mark1(X1), mark1(X2))
A__PI1(X) -> MARK1(X)
A__2NDSPOS2(s1(N), cons2(X, Z)) -> MARK1(Z)
MARK1(s1(X)) -> MARK1(X)
MARK1(rcons2(X1, X2)) -> MARK1(X2)
MARK1(2ndspos2(X1, X2)) -> A__2NDSPOS2(mark1(X1), mark1(X2))
MARK1(2ndsneg2(X1, X2)) -> A__2NDSNEG2(mark1(X1), mark1(X2))
A__2NDSPOS2(s1(N), cons2(X, Z)) -> MARK1(N)
MARK1(pi1(X)) -> MARK1(X)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(N)
A__SQUARE1(X) -> MARK1(X)
A__FROM1(X) -> MARK1(X)
MARK1(plus2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Y)
A__TIMES2(s1(X), Y) -> A__PLUS2(mark1(Y), a__times2(mark1(X), mark1(Y)))
MARK1(times2(X1, X2)) -> MARK1(X1)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> MARK1(N)
A__2NDSNEG2(s1(N), cons2(X, Z)) -> MARK1(Z)
MARK1(cons22(X1, X2)) -> MARK1(X2)
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Z)
A__PLUS2(s1(X), Y) -> A__PLUS2(mark1(X), mark1(Y))
MARK1(from1(X)) -> MARK1(X)
A__PI1(X) -> A__FROM1(0)
MARK1(from1(X)) -> A__FROM1(mark1(X))
MARK1(pi1(X)) -> A__PI1(mark1(X))
MARK1(cons2(X1, X2)) -> MARK1(X1)
A__SQUARE1(X) -> A__TIMES2(mark1(X), mark1(X))
A__PLUS2(0, Y) -> MARK1(Y)
MARK1(2ndspos2(X1, X2)) -> MARK1(X2)
A__PLUS2(s1(X), Y) -> MARK1(X)
MARK1(square1(X)) -> MARK1(X)
MARK1(2ndsneg2(X1, X2)) -> MARK1(X1)
MARK1(square1(X)) -> A__SQUARE1(mark1(X))
A__PLUS2(s1(X), Y) -> MARK1(Y)
MARK1(2ndsneg2(X1, X2)) -> MARK1(X2)
A__2NDSPOS2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Y)
A__2NDSNEG2(s1(N), cons22(X, cons2(Y, Z))) -> MARK1(Z)
A__TIMES2(s1(X), Y) -> MARK1(Y)

The TRS R consists of the following rules:

a__from1(X) -> cons2(mark1(X), from1(s1(X)))
a__2ndspos2(0, Z) -> rnil
a__2ndspos2(s1(N), cons2(X, Z)) -> a__2ndspos2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndspos2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(posrecip1(mark1(Y)), a__2ndsneg2(mark1(N), mark1(Z)))
a__2ndsneg2(0, Z) -> rnil
a__2ndsneg2(s1(N), cons2(X, Z)) -> a__2ndsneg2(s1(mark1(N)), cons22(X, mark1(Z)))
a__2ndsneg2(s1(N), cons22(X, cons2(Y, Z))) -> rcons2(negrecip1(mark1(Y)), a__2ndspos2(mark1(N), mark1(Z)))
a__pi1(X) -> a__2ndspos2(mark1(X), a__from1(0))
a__plus2(0, Y) -> mark1(Y)
a__plus2(s1(X), Y) -> s1(a__plus2(mark1(X), mark1(Y)))
a__times2(0, Y) -> 0
a__times2(s1(X), Y) -> a__plus2(mark1(Y), a__times2(mark1(X), mark1(Y)))
a__square1(X) -> a__times2(mark1(X), mark1(X))
mark1(from1(X)) -> a__from1(mark1(X))
mark1(2ndspos2(X1, X2)) -> a__2ndspos2(mark1(X1), mark1(X2))
mark1(2ndsneg2(X1, X2)) -> a__2ndsneg2(mark1(X1), mark1(X2))
mark1(pi1(X)) -> a__pi1(mark1(X))
mark1(plus2(X1, X2)) -> a__plus2(mark1(X1), mark1(X2))
mark1(times2(X1, X2)) -> a__times2(mark1(X1), mark1(X2))
mark1(square1(X)) -> a__square1(mark1(X))
mark1(0) -> 0
mark1(s1(X)) -> s1(mark1(X))
mark1(posrecip1(X)) -> posrecip1(mark1(X))
mark1(negrecip1(X)) -> negrecip1(mark1(X))
mark1(nil) -> nil
mark1(cons2(X1, X2)) -> cons2(mark1(X1), X2)
mark1(cons22(X1, X2)) -> cons22(X1, mark1(X2))
mark1(rnil) -> rnil
mark1(rcons2(X1, X2)) -> rcons2(mark1(X1), mark1(X2))
a__from1(X) -> from1(X)
a__2ndspos2(X1, X2) -> 2ndspos2(X1, X2)
a__2ndsneg2(X1, X2) -> 2ndsneg2(X1, X2)
a__pi1(X) -> pi1(X)
a__plus2(X1, X2) -> plus2(X1, X2)
a__times2(X1, X2) -> times2(X1, X2)
a__square1(X) -> square1(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.